T:Type, R:(TT).
WellFnd{i}(T;x,y.R(x,y))
 (x, y:T. Dec(R(x,y)))
 (y:T. L:T List. (x:T. (R(x,y))  (x  L)))
 (y:T. x:T. ((R^*)(x,y) & (z:T. (R(z,x))))) 

latex

Definitions	f(a), Void, x:AB(x), P  Q, False, A, x:A. B(x), P & Q, R^*, x:A  B(x), x:A. B(x), t  T, Type, {T}, WellFnd{i}(A;x,y.R(x;y)), Dec(P), s = t, a < b, (x  l), x. t(x), A c B, P  Q, type List, , True, x.A(x), x f y, R^+
Lemmas	rel-rel-plus, wellfounded-minimal